\begin{tabbing}
R{-}compat\=\{i:l\}\+
\\[0ex]($A$; $B$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= Rplus?($A$)\+\+
\\[0ex]then R{-}compat\{i:l\}(Rplus{-}left($A$); $B$) $\wedge$ R{-}compat\{i:l\}(Rplus{-}right($A$); $B$)
\-\\[0ex]if\= Rplus?($B$)\+
\\[0ex]then R{-}compat\{i:l\}($A$; Rplus{-}left($B$)) $\wedge$ R{-}compat\{i:l\}($A$; Rplus{-}right($B$))
\-\\[0ex]if\= Rnone?($A$)\+
\\[0ex]then True
\-\\[0ex]if\= Rnone?($B$)\+
\\[0ex]then True
\-\\[0ex]if\= eq\_id(R{-}loc($A$); R{-}loc($B$))\+
\\[0ex]then \=(fpf{-}compatible(Id; $x$.Type; id{-}deq; Rds($A$); Rds($B$))\+
\\[0ex]$\wedge$ fpf{-}compatible(Knd; $x$.Type; Kind{-}deq; Rda($A$); Rda($B$)))
\\[0ex]$\wedge$ \=if eq\_bd(R{-}base{-}domain($A$); R{-}base{-}domain($B$))\+
\\[0ex]then $A$ = $B$
\\[0ex]else R{-}frame{-}compat($A$; $B$) $\wedge$ R{-}frame{-}compat($B$; $A$) $\wedge$ R{-}discrete\_compat($A$; $B$)
\\[0ex]fi 
\-\-\-\\[0ex]else R{-}interface{-}compat($A$; $B$) $\wedge$ R{-}interface{-}compat($B$; $A$)
\\[0ex]fi 
\\[0ex]
\-\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]R{-}compat\=\{i:l\}\+
\\[0ex]($A$; $B$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= Rplus?($A$)\+\+
\\[0ex]then R{-}compat\{i:l\}(Rplus{-}left($A$); $B$) $\wedge$ R{-}compat\{i:l\}(Rplus{-}right($A$); $B$)
\-\\[0ex]if\= Rplus?($B$)\+
\\[0ex]then R{-}compat\{i:l\}($A$; Rplus{-}left($B$)) $\wedge$ R{-}compat\{i:l\}($A$; Rplus{-}right($B$))
\-\\[0ex]if\= Rnone?($A$)\+
\\[0ex]then True
\-\\[0ex]if\= Rnone?($B$)\+
\\[0ex]then True
\-\\[0ex]if\= eq\_id(R{-}loc($A$); R{-}loc($B$))\+
\\[0ex]then \=(fpf{-}compatible(Id; $x$.Type\{i\}; id{-}deq; Rds($A$); Rds($B$))\+
\\[0ex]$\wedge$ fpf{-}compatible(Knd; $x$.Type\{i\}; Kind{-}deq; Rda($A$); Rda($B$)))
\\[0ex]$\wedge$ \=if eq\_bd(R{-}base{-}domain($A$); R{-}base{-}domain($B$))\+
\\[0ex]then $A$ = $B$ $\in$ es\_realizer\{i:l\}
\\[0ex]else R{-}frame{-}compat($A$; $B$) $\wedge$ R{-}frame{-}compat($B$; $A$) $\wedge$ R{-}discrete\_compat($A$; $B$)
\\[0ex]fi 
\-\-\-\\[0ex]else R{-}interface{-}compat($A$; $B$) $\wedge$ R{-}interface{-}compat($B$; $A$)
\\[0ex]fi 
\-\\[0ex]\emph{(recursive)}
\end{tabbing}